Left Termination of the query pattern queens_in_1(a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

queens(Y) :- ','(perm(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y), safe(Y)).
perm([], []).
perm(.(X, Y), .(V, Res)) :- ','(delete(V, .(X, Y), Rest), perm(Rest, Res)).
delete(X, .(X, Y), Y).
delete(X, .(F, T), .(F, R)) :- delete(X, T, R).
safe([]).
safe(.(X, Y)) :- ','(noattack(X, Y, s(0)), safe(Y)).
noattack(X, [], N).
noattack(X, .(F, T), N) :- ','(notEq(X, F), ','(add(F, N, FplusN), ','(notEq(X, FplusN), ','(add(X, N, XplusN), ','(notEq(F, XplusN), noattack(X, T, s(N))))))).
add(0, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
notEq(0, s(X)).
notEq(s(X), 0).
notEq(s(X), s(Y)) :- notEq(X, Y).

Queries:

queens(a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

QUEENS_IN(Y) → U11(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
QUEENS_IN(Y) → PERM_IN(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)
PERM_IN(.(X, Y), .(V, Res)) → U31(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
PERM_IN(.(X, Y), .(V, Res)) → DELETE_IN(V, .(X, Y), Rest)
DELETE_IN(X, .(F, T), .(F, R)) → U51(X, F, T, R, delete_in(X, T, R))
DELETE_IN(X, .(F, T), .(F, R)) → DELETE_IN(X, T, R)
U31(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U41(X, Y, V, Res, perm_in(Rest, Res))
U31(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → PERM_IN(Rest, Res)
U11(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U21(Y, safe_in(Y))
U11(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → SAFE_IN(Y)
SAFE_IN(.(X, Y)) → U61(X, Y, noattack_in(X, Y, s(0)))
SAFE_IN(.(X, Y)) → NOATTACK_IN(X, Y, s(0))
NOATTACK_IN(X, .(F, T), N) → U81(X, F, T, N, notEq_in(X, F))
NOATTACK_IN(X, .(F, T), N) → NOTEQ_IN(X, F)
NOTEQ_IN(s(X), s(Y)) → U151(X, Y, notEq_in(X, Y))
NOTEQ_IN(s(X), s(Y)) → NOTEQ_IN(X, Y)
U81(X, F, T, N, notEq_out(X, F)) → U91(X, F, T, N, add_in(F, N, FplusN))
U81(X, F, T, N, notEq_out(X, F)) → ADD_IN(F, N, FplusN)
ADD_IN(s(X), Y, s(Z)) → U141(X, Y, Z, add_in(X, Y, Z))
ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)
U91(X, F, T, N, add_out(F, N, FplusN)) → U101(X, F, T, N, FplusN, notEq_in(X, FplusN))
U91(X, F, T, N, add_out(F, N, FplusN)) → NOTEQ_IN(X, FplusN)
U101(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U111(X, F, T, N, FplusN, add_in(X, N, XplusN))
U101(X, F, T, N, FplusN, notEq_out(X, FplusN)) → ADD_IN(X, N, XplusN)
U111(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U121(X, F, T, N, notEq_in(F, XplusN))
U111(X, F, T, N, FplusN, add_out(X, N, XplusN)) → NOTEQ_IN(F, XplusN)
U121(X, F, T, N, notEq_out(F, XplusN)) → U131(X, F, T, N, noattack_in(X, T, s(N)))
U121(X, F, T, N, notEq_out(F, XplusN)) → NOATTACK_IN(X, T, s(N))
U61(X, Y, noattack_out(X, Y, s(0))) → U71(X, Y, safe_in(Y))
U61(X, Y, noattack_out(X, Y, s(0))) → SAFE_IN(Y)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
U101(x1, x2, x3, x4, x5, x6)  =  U101(x1, x2, x3, x4, x6)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)
U71(x1, x2, x3)  =  U71(x3)
U141(x1, x2, x3, x4)  =  U141(x4)
U31(x1, x2, x3, x4, x5)  =  U31(x5)
U91(x1, x2, x3, x4, x5)  =  U91(x1, x2, x3, x4, x5)
SAFE_IN(x1)  =  SAFE_IN(x1)
PERM_IN(x1, x2)  =  PERM_IN(x1)
U21(x1, x2)  =  U21(x1, x2)
QUEENS_IN(x1)  =  QUEENS_IN
U61(x1, x2, x3)  =  U61(x2, x3)
NOATTACK_IN(x1, x2, x3)  =  NOATTACK_IN(x1, x2, x3)
U51(x1, x2, x3, x4, x5)  =  U51(x2, x5)
U111(x1, x2, x3, x4, x5, x6)  =  U111(x1, x2, x3, x4, x6)
U41(x1, x2, x3, x4, x5)  =  U41(x3, x5)
U11(x1, x2)  =  U11(x2)
U131(x1, x2, x3, x4, x5)  =  U131(x5)
U81(x1, x2, x3, x4, x5)  =  U81(x1, x2, x3, x4, x5)
U121(x1, x2, x3, x4, x5)  =  U121(x1, x3, x4, x5)
NOTEQ_IN(x1, x2)  =  NOTEQ_IN(x1, x2)
U151(x1, x2, x3)  =  U151(x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

QUEENS_IN(Y) → U11(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
QUEENS_IN(Y) → PERM_IN(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)
PERM_IN(.(X, Y), .(V, Res)) → U31(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
PERM_IN(.(X, Y), .(V, Res)) → DELETE_IN(V, .(X, Y), Rest)
DELETE_IN(X, .(F, T), .(F, R)) → U51(X, F, T, R, delete_in(X, T, R))
DELETE_IN(X, .(F, T), .(F, R)) → DELETE_IN(X, T, R)
U31(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U41(X, Y, V, Res, perm_in(Rest, Res))
U31(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → PERM_IN(Rest, Res)
U11(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U21(Y, safe_in(Y))
U11(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → SAFE_IN(Y)
SAFE_IN(.(X, Y)) → U61(X, Y, noattack_in(X, Y, s(0)))
SAFE_IN(.(X, Y)) → NOATTACK_IN(X, Y, s(0))
NOATTACK_IN(X, .(F, T), N) → U81(X, F, T, N, notEq_in(X, F))
NOATTACK_IN(X, .(F, T), N) → NOTEQ_IN(X, F)
NOTEQ_IN(s(X), s(Y)) → U151(X, Y, notEq_in(X, Y))
NOTEQ_IN(s(X), s(Y)) → NOTEQ_IN(X, Y)
U81(X, F, T, N, notEq_out(X, F)) → U91(X, F, T, N, add_in(F, N, FplusN))
U81(X, F, T, N, notEq_out(X, F)) → ADD_IN(F, N, FplusN)
ADD_IN(s(X), Y, s(Z)) → U141(X, Y, Z, add_in(X, Y, Z))
ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)
U91(X, F, T, N, add_out(F, N, FplusN)) → U101(X, F, T, N, FplusN, notEq_in(X, FplusN))
U91(X, F, T, N, add_out(F, N, FplusN)) → NOTEQ_IN(X, FplusN)
U101(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U111(X, F, T, N, FplusN, add_in(X, N, XplusN))
U101(X, F, T, N, FplusN, notEq_out(X, FplusN)) → ADD_IN(X, N, XplusN)
U111(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U121(X, F, T, N, notEq_in(F, XplusN))
U111(X, F, T, N, FplusN, add_out(X, N, XplusN)) → NOTEQ_IN(F, XplusN)
U121(X, F, T, N, notEq_out(F, XplusN)) → U131(X, F, T, N, noattack_in(X, T, s(N)))
U121(X, F, T, N, notEq_out(F, XplusN)) → NOATTACK_IN(X, T, s(N))
U61(X, Y, noattack_out(X, Y, s(0))) → U71(X, Y, safe_in(Y))
U61(X, Y, noattack_out(X, Y, s(0))) → SAFE_IN(Y)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
U101(x1, x2, x3, x4, x5, x6)  =  U101(x1, x2, x3, x4, x6)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)
U71(x1, x2, x3)  =  U71(x3)
U141(x1, x2, x3, x4)  =  U141(x4)
U31(x1, x2, x3, x4, x5)  =  U31(x5)
U91(x1, x2, x3, x4, x5)  =  U91(x1, x2, x3, x4, x5)
SAFE_IN(x1)  =  SAFE_IN(x1)
PERM_IN(x1, x2)  =  PERM_IN(x1)
U21(x1, x2)  =  U21(x1, x2)
QUEENS_IN(x1)  =  QUEENS_IN
U61(x1, x2, x3)  =  U61(x2, x3)
NOATTACK_IN(x1, x2, x3)  =  NOATTACK_IN(x1, x2, x3)
U51(x1, x2, x3, x4, x5)  =  U51(x2, x5)
U111(x1, x2, x3, x4, x5, x6)  =  U111(x1, x2, x3, x4, x6)
U41(x1, x2, x3, x4, x5)  =  U41(x3, x5)
U11(x1, x2)  =  U11(x2)
U131(x1, x2, x3, x4, x5)  =  U131(x5)
U81(x1, x2, x3, x4, x5)  =  U81(x1, x2, x3, x4, x5)
U121(x1, x2, x3, x4, x5)  =  U121(x1, x3, x4, x5)
NOTEQ_IN(x1, x2)  =  NOTEQ_IN(x1, x2)
U151(x1, x2, x3)  =  U151(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 6 SCCs with 17 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y) → ADD_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NOTEQ_IN(s(X), s(Y)) → NOTEQ_IN(X, Y)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
NOTEQ_IN(x1, x2)  =  NOTEQ_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NOTEQ_IN(s(X), s(Y)) → NOTEQ_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

NOTEQ_IN(s(X), s(Y)) → NOTEQ_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U121(X, F, T, N, notEq_out(F, XplusN)) → NOATTACK_IN(X, T, s(N))
U91(X, F, T, N, add_out(F, N, FplusN)) → U101(X, F, T, N, FplusN, notEq_in(X, FplusN))
U111(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U121(X, F, T, N, notEq_in(F, XplusN))
NOATTACK_IN(X, .(F, T), N) → U81(X, F, T, N, notEq_in(X, F))
U81(X, F, T, N, notEq_out(X, F)) → U91(X, F, T, N, add_in(F, N, FplusN))
U101(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U111(X, F, T, N, FplusN, add_in(X, N, XplusN))

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
U101(x1, x2, x3, x4, x5, x6)  =  U101(x1, x2, x3, x4, x6)
U91(x1, x2, x3, x4, x5)  =  U91(x1, x2, x3, x4, x5)
NOATTACK_IN(x1, x2, x3)  =  NOATTACK_IN(x1, x2, x3)
U111(x1, x2, x3, x4, x5, x6)  =  U111(x1, x2, x3, x4, x6)
U81(x1, x2, x3, x4, x5)  =  U81(x1, x2, x3, x4, x5)
U121(x1, x2, x3, x4, x5)  =  U121(x1, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U121(X, F, T, N, notEq_out(F, XplusN)) → NOATTACK_IN(X, T, s(N))
U91(X, F, T, N, add_out(F, N, FplusN)) → U101(X, F, T, N, FplusN, notEq_in(X, FplusN))
U111(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U121(X, F, T, N, notEq_in(F, XplusN))
NOATTACK_IN(X, .(F, T), N) → U81(X, F, T, N, notEq_in(X, F))
U81(X, F, T, N, notEq_out(X, F)) → U91(X, F, T, N, add_in(F, N, FplusN))
U101(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U111(X, F, T, N, FplusN, add_in(X, N, XplusN))

The TRS R consists of the following rules:

notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U101(x1, x2, x3, x4, x5, x6)  =  U101(x1, x2, x3, x4, x6)
U91(x1, x2, x3, x4, x5)  =  U91(x1, x2, x3, x4, x5)
NOATTACK_IN(x1, x2, x3)  =  NOATTACK_IN(x1, x2, x3)
U111(x1, x2, x3, x4, x5, x6)  =  U111(x1, x2, x3, x4, x6)
U81(x1, x2, x3, x4, x5)  =  U81(x1, x2, x3, x4, x5)
U121(x1, x2, x3, x4, x5)  =  U121(x1, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U111(X, F, T, N, add_out(XplusN)) → U121(X, T, N, notEq_in(F, XplusN))
U81(X, F, T, N, notEq_out) → U91(X, F, T, N, add_in(F, N))
U91(X, F, T, N, add_out(FplusN)) → U101(X, F, T, N, notEq_in(X, FplusN))
U121(X, T, N, notEq_out) → NOATTACK_IN(X, T, s(N))
U101(X, F, T, N, notEq_out) → U111(X, F, T, N, add_in(X, N))
NOATTACK_IN(X, .(F, T), N) → U81(X, F, T, N, notEq_in(X, F))

The TRS R consists of the following rules:

notEq_in(s(X), s(Y)) → U15(notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out
notEq_in(0, s(X)) → notEq_out
add_in(s(X), Y) → U14(add_in(X, Y))
add_in(0, X) → add_out(X)
U15(notEq_out) → notEq_out
U14(add_out(Z)) → add_out(s(Z))

The set Q consists of the following terms:

notEq_in(x0, x1)
add_in(x0, x1)
U15(x0)
U14(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SAFE_IN(.(X, Y)) → U61(X, Y, noattack_in(X, Y, s(0)))
U61(X, Y, noattack_out(X, Y, s(0))) → SAFE_IN(Y)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
SAFE_IN(x1)  =  SAFE_IN(x1)
U61(x1, x2, x3)  =  U61(x2, x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SAFE_IN(.(X, Y)) → U61(X, Y, noattack_in(X, Y, s(0)))
U61(X, Y, noattack_out(X, Y, s(0))) → SAFE_IN(Y)

The TRS R consists of the following rules:

noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
noattack_in(X, [], N) → noattack_out(X, [], N)
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
SAFE_IN(x1)  =  SAFE_IN(x1)
U61(x1, x2, x3)  =  U61(x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SAFE_IN(.(X, Y)) → U61(Y, noattack_in(X, Y, s(0)))
U61(Y, noattack_out) → SAFE_IN(Y)

The TRS R consists of the following rules:

noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
noattack_in(X, [], N) → noattack_out
U8(X, F, T, N, notEq_out) → U9(X, F, T, N, add_in(F, N))
notEq_in(s(X), s(Y)) → U15(notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out
notEq_in(0, s(X)) → notEq_out
U9(X, F, T, N, add_out(FplusN)) → U10(X, F, T, N, notEq_in(X, FplusN))
U15(notEq_out) → notEq_out
add_in(s(X), Y) → U14(add_in(X, Y))
add_in(0, X) → add_out(X)
U10(X, F, T, N, notEq_out) → U11(X, F, T, N, add_in(X, N))
U14(add_out(Z)) → add_out(s(Z))
U11(X, F, T, N, add_out(XplusN)) → U12(X, T, N, notEq_in(F, XplusN))
U12(X, T, N, notEq_out) → U13(noattack_in(X, T, s(N)))
U13(noattack_out) → noattack_out

The set Q consists of the following terms:

noattack_in(x0, x1, x2)
U8(x0, x1, x2, x3, x4)
notEq_in(x0, x1)
U9(x0, x1, x2, x3, x4)
U15(x0)
add_in(x0, x1)
U10(x0, x1, x2, x3, x4)
U14(x0)
U11(x0, x1, x2, x3, x4)
U12(x0, x1, x2, x3)
U13(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(F, T), .(F, R)) → DELETE_IN(X, T, R)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(F, T), .(F, R)) → DELETE_IN(X, T, R)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
DELETE_IN(x1, x2, x3)  =  DELETE_IN(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

DELETE_IN(.(F, T)) → DELETE_IN(T)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

PERM_IN(.(X, Y), .(V, Res)) → U31(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
U31(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → PERM_IN(Rest, Res)

The TRS R consists of the following rules:

queens_in(Y) → U1(Y, perm_in(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in(.(X, Y), .(V, Res)) → U3(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))
U3(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → U4(X, Y, V, Res, perm_in(Rest, Res))
perm_in([], []) → perm_out([], [])
U4(X, Y, V, Res, perm_out(Rest, Res)) → perm_out(.(X, Y), .(V, Res))
U1(Y, perm_out(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2(Y, safe_in(Y))
safe_in(.(X, Y)) → U6(X, Y, noattack_in(X, Y, s(0)))
noattack_in(X, .(F, T), N) → U8(X, F, T, N, notEq_in(X, F))
notEq_in(s(X), s(Y)) → U15(X, Y, notEq_in(X, Y))
notEq_in(s(X), 0) → notEq_out(s(X), 0)
notEq_in(0, s(X)) → notEq_out(0, s(X))
U15(X, Y, notEq_out(X, Y)) → notEq_out(s(X), s(Y))
U8(X, F, T, N, notEq_out(X, F)) → U9(X, F, T, N, add_in(F, N, FplusN))
add_in(s(X), Y, s(Z)) → U14(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
U14(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U9(X, F, T, N, add_out(F, N, FplusN)) → U10(X, F, T, N, FplusN, notEq_in(X, FplusN))
U10(X, F, T, N, FplusN, notEq_out(X, FplusN)) → U11(X, F, T, N, FplusN, add_in(X, N, XplusN))
U11(X, F, T, N, FplusN, add_out(X, N, XplusN)) → U12(X, F, T, N, notEq_in(F, XplusN))
U12(X, F, T, N, notEq_out(F, XplusN)) → U13(X, F, T, N, noattack_in(X, T, s(N)))
noattack_in(X, [], N) → noattack_out(X, [], N)
U13(X, F, T, N, noattack_out(X, T, s(N))) → noattack_out(X, .(F, T), N)
U6(X, Y, noattack_out(X, Y, s(0))) → U7(X, Y, safe_in(Y))
safe_in([]) → safe_out([])
U7(X, Y, safe_out(Y)) → safe_out(.(X, Y))
U2(Y, safe_out(Y)) → queens_out(Y)

The argument filtering Pi contains the following mapping:
queens_in(x1)  =  queens_in
U1(x1, x2)  =  U1(x2)
perm_in(x1, x2)  =  perm_in(x1)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
[]  =  []
U3(x1, x2, x3, x4, x5)  =  U3(x5)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U4(x1, x2, x3, x4, x5)  =  U4(x3, x5)
perm_out(x1, x2)  =  perm_out(x2)
U2(x1, x2)  =  U2(x1, x2)
safe_in(x1)  =  safe_in(x1)
U6(x1, x2, x3)  =  U6(x2, x3)
noattack_in(x1, x2, x3)  =  noattack_in(x1, x2, x3)
U8(x1, x2, x3, x4, x5)  =  U8(x1, x2, x3, x4, x5)
notEq_in(x1, x2)  =  notEq_in(x1, x2)
U15(x1, x2, x3)  =  U15(x3)
notEq_out(x1, x2)  =  notEq_out
U9(x1, x2, x3, x4, x5)  =  U9(x1, x2, x3, x4, x5)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U14(x1, x2, x3, x4)  =  U14(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U10(x1, x2, x3, x4, x5, x6)  =  U10(x1, x2, x3, x4, x6)
U11(x1, x2, x3, x4, x5, x6)  =  U11(x1, x2, x3, x4, x6)
U12(x1, x2, x3, x4, x5)  =  U12(x1, x3, x4, x5)
U13(x1, x2, x3, x4, x5)  =  U13(x5)
noattack_out(x1, x2, x3)  =  noattack_out
U7(x1, x2, x3)  =  U7(x3)
safe_out(x1)  =  safe_out
queens_out(x1)  =  queens_out(x1)
U31(x1, x2, x3, x4, x5)  =  U31(x5)
PERM_IN(x1, x2)  =  PERM_IN(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

PERM_IN(.(X, Y), .(V, Res)) → U31(X, Y, V, Res, delete_in(V, .(X, Y), Rest))
U31(X, Y, V, Res, delete_out(V, .(X, Y), Rest)) → PERM_IN(Rest, Res)

The TRS R consists of the following rules:

delete_in(X, .(F, T), .(F, R)) → U5(X, F, T, R, delete_in(X, T, R))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U5(X, F, T, R, delete_out(X, T, R)) → delete_out(X, .(F, T), .(F, R))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
delete_in(x1, x2, x3)  =  delete_in(x2)
U5(x1, x2, x3, x4, x5)  =  U5(x2, x5)
delete_out(x1, x2, x3)  =  delete_out(x1, x3)
U31(x1, x2, x3, x4, x5)  =  U31(x5)
PERM_IN(x1, x2)  =  PERM_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

U31(delete_out(V, Rest)) → PERM_IN(Rest)
PERM_IN(.(X, Y)) → U31(delete_in(.(X, Y)))

The TRS R consists of the following rules:

delete_in(.(F, T)) → U5(F, delete_in(T))
delete_in(.(X, Y)) → delete_out(X, Y)
U5(F, delete_out(X, R)) → delete_out(X, .(F, R))

The set Q consists of the following terms:

delete_in(x0)
U5(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

PERM_IN(.(X, Y)) → U31(delete_in(.(X, Y)))

Strictly oriented rules of the TRS R:

delete_in(.(X, Y)) → delete_out(X, Y)

Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 1 + x1 + x2   
POL(PERM_IN(x1)) = 2 + 2·x1   
POL(U31(x1)) = x1   
POL(U5(x1, x2)) = 2 + 2·x1 + x2   
POL(delete_in(x1)) = 1 + 2·x1   
POL(delete_out(x1, x2)) = 2 + 2·x1 + 2·x2   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                          ↳ QDP
                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U31(delete_out(V, Rest)) → PERM_IN(Rest)

The TRS R consists of the following rules:

delete_in(.(F, T)) → U5(F, delete_in(T))
U5(F, delete_out(X, R)) → delete_out(X, .(F, R))

The set Q consists of the following terms:

delete_in(x0)
U5(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.